The present invention relates to a system and method for test generation with dynamic constraints, and in particular, to a system and method for resolving constraints in multiple domains by creating a set of instructions which provide one or more specific, random solutions when executed.
Design verification is the process of determining whether an integrated circuit, board, or system-level architecture, exactly implements the requirements defined by the specification of the architecture for that device. Design verification for a device under test (DUT) may be performed on the actual device, or on a simulation model of the device. For the purposes of explanation only and without intending to be limiting in any way, the following discussion centers upon testing that is performed on simulation models of the device.
As designs for different types of devices and device architectures become more complex, the likelihood of design errors increases. However, design verification also becomes more difficult and time consuming as the simulation models of the design of the device also become more complex to prepare and to test.
The process of verifying a design through a simulation model of the device is aided by the availability of hardware description languages such as Verilog and VHDL. These languages are designed to describe hardware at higher levels of abstraction than gates or transistors. The resultant simulated model of the device can receive input stimuli in the form of test vectors, which are a string of binary values applied to the input of a circuit. The simulated model then produces results, which are checked against the expected results for the particular design of the device. However, these languages are typically not designed for actual verification. Therefore, the verification engineer must write additional programming code in order to interface with the models described by these hardware description languages in order to perform design verification of the device.
Within the area of testing and verification environments, both static and dynamic testing and verification environments traditionally have been implemented with fixed-vector or pre-generation input. More recently, a more powerful and more sophisticated implementation uses test generation to produce the DUT input in concurrence with the simulation of the model of the DUT.
A useful and efficient type of testing is a dynamic testing environment. For this type of environment, a set of programming instructions is written to generate the test vectors in concurrence with the simulation of the model of the DUT with potential inputs from feedback from the simulated device. This procedure enables directed random generation to be performed and to be sensitive to effects uncovered during the test itself on the state of the simulation model of the device. Thus dynamic test generation clearly has many advantages for design verification.
One example of such a test generator is disclosed in U.S. Pat. No. 6,182,258, issued Jan. 30, 2001 (application Ser. No. 09/020,792, filed on Feb. 6, 1998) and U.S. Pat. No. 6,684,359, issued Jan. 27, 2004, each incorporated by reference as if fully set forth herein. This test generation procedure interacts with, and sits as a higher level over, such hardware description languages as Verilog and VHDL. The test generation procedure is written in a hardware-oriented verification specific object-oriented programming language. This language is used to write various verification environments, which then can be used to automatically create a device verification test managed by a test generator module. A wide variety of design environments can be tested and verified with this language. Thus, the procedure is generalizable, yet is also simple to program and to debug by the engineer. The language features a number of elements such as “structs” for more richly and efficiently describing the design of the device to be simulated by the model.
Currently available commercial systems, such as Specman Elite software available from Cadence Design Systems, support resolving dynamic constraints through a specific, correct solution, the specific solution random within but compliant with the constraints. The solution is created by executing a specific set of instructions. In the course of testing a simulation, large numbers of such solutions can be generated and tested in the test environment. A typical test may utilize many thousands of specific sets of values. This tool provides a good, random solution for dynamic constraints in a reasonable processing time, and can react dynamically on the same time scale as the time period that is actually required for simulation.
A problem with existing solutions is that certain constraints are best resolved (or solved) using one type of a solver, while other constraints are best resolved with a different solver that is itself not very efficient for resolving the first type of constraints. For example, constraints that are primarily arithmetic are well matched to an arithmetic solver using, for example, range lists, such as those described in U.S. Pat. No. 6,182,258. Arithmetic constraints include linear programming or differential equations, or even simple relationships like greater than, less than, equal to, sum or difference of multiple values (variable or constant), and so on. In similar manner, constraints that are primarily binary are well matched to a binary solver using, for example binary decision diagrams (BDD). Unfortunately, binary solvers are generally not very useful for resolving arithmetic constraints, and arithmetic solvers are not well suited to resolving binary constraints. This means that the solver may (but may not) be able to present a useable solution, and in any event the process of resolving non-compatible constraints is at best slow and/or inefficient. Another useful solver known in the art is a SAT (satisfiability) engine. This solver is well adapted to constraints that have certain mixes of binary and arithmetic properties, but even here the solver is not optimized for binary or arithmetic constraints by themselves, and thus is itself not as efficient as a binary solver for primarily binary constraints, or as efficient as an arithmetic solver for primarily arithmetic constraints.
A major problem with any one of these solvers is that the constraints in a given design often contain a mix of constraints that are not entirely well suited for resolution with any one solver. It would be helpful to match certain types of constraints with an appropriate solver, and to match other constraints in the same design with a different appropriate solver, thus providing to each of the constraints at hand a solver well adapted to that constraint. Combining two or more solvers in a modular fashion for the purpose of test generation is neither straightforward nor simple, and has not been done before. For example, coordination of solver to constraint and a variety of run-time issues need to be addressed.
Multiple solvers have been used in model checking, however this is a very different application with different requirements and results. In U.S. Pat. No. 6,698,003, an IBM patent, Baumgartner et al discuss multi-engine model checking for verification. The “verification problem” mentioned in the patent is a model checking problem namely, “Does a property hold over a design?” It is not about constraint resolution. See also Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 21, NO. 12, DECEMBER 2002. This is an overview paper describing the usefulness of a multi-engine approach across CAD applications. This also does not disclose constraint resolution according to the present invention.
Therefore there is an unmet need for, and it would be highly useful to have, a system and method for resolving constraints in multiple domains to make available one or preferably more than one random but correct, specific solutions that can be utilized in a test environment.